In this direction, a number of techniques from the field of AI have been applied to BPMSs with the aim of increasing the degree of automated process adaptation (Marrella, 2018, 2019). In (Gajewski et al., 2005; Ferreira and Ferreira, 2006; Marrella and Lespérance, 2013, 2017), if a task failure occurs at run-time and leads to a process goal violation, a new complete process definition that complies with the goal is generated relying on a partial-order AI planner. As a side effect, this often significantly modifies the assignment of tasks to process participants. The work (Bucchiarone et al., 2011) proposes a goal-driven approach to adapt processes to run-time context changes. Process and context changes that prevent goal achievement are specified at design-time and recovery strategies are built at run-time through an adaptation mechanism based on service composition via AI planning.

FSCQ is the first file system with a machine-checkable proof that its implementation meets a specification, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover its state correctly without losing data. To state FSCQ's theorems, this paper introduces the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers. This paper describes Crash Hoare logic (CHL), which allows developers to write specifications for crash-safe storage systems and also prove them correct. "Correct" means that, if a computer crashes due to a power failure or other fail-stop fault and subsequently reboots, the storage system will recover to a state consistent with its specification (e.g., POSIX17). For example, after recovery, either all disk writes from a file-system call will be on disk, or none will be. Using CHL we write a simple specification for a subset of POSIX and build the FSCQ certified file system, which comes with a machine-checkable proof that its implementation matches the specification. Proving the correctness of a file system implementation is important, because existing file systems have a long history of bugs both in normal operation and in handling crashes.24